/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.checker;

import java.util.Arrays;
import java.util.Collections;
import java.util.List;
import java.util.Map;

import org.eclipse.jdt.core.dom.ASTNode;
import org.eclipse.jdt.core.dom.ASTVisitor;
import org.eclipse.jdt.core.dom.ArrayAccess;
import org.eclipse.jdt.core.dom.ArrayCreation;
import org.eclipse.jdt.core.dom.ArrayInitializer;
import org.eclipse.jdt.core.dom.Assignment;
import org.eclipse.jdt.core.dom.Block;
import org.eclipse.jdt.core.dom.BooleanLiteral;
import org.eclipse.jdt.core.dom.CastExpression;
import org.eclipse.jdt.core.dom.ChildListPropertyDescriptor;
import org.eclipse.jdt.core.dom.ChildPropertyDescriptor;
import org.eclipse.jdt.core.dom.ClassInstanceCreation;
import org.eclipse.jdt.core.dom.ConditionalExpression;
import org.eclipse.jdt.core.dom.ConstructorInvocation;
import org.eclipse.jdt.core.dom.EnhancedForStatement;
import org.eclipse.jdt.core.dom.Expression;
import org.eclipse.jdt.core.dom.ExpressionStatement;
import org.eclipse.jdt.core.dom.ForStatement;
import org.eclipse.jdt.core.dom.IBinding;
import org.eclipse.jdt.core.dom.IMethodBinding;
import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.IfStatement;
import org.eclipse.jdt.core.dom.LabeledStatement;
import org.eclipse.jdt.core.dom.MethodDeclaration;
import org.eclipse.jdt.core.dom.MethodInvocation;
import org.eclipse.jdt.core.dom.Modifier;
import org.eclipse.jdt.core.dom.NullLiteral;
import org.eclipse.jdt.core.dom.NumberLiteral;
import org.eclipse.jdt.core.dom.ParenthesizedExpression;
import org.eclipse.jdt.core.dom.ReturnStatement;
import org.eclipse.jdt.core.dom.SimpleName;
import org.eclipse.jdt.core.dom.SingleVariableDeclaration;
import org.eclipse.jdt.core.dom.StringLiteral;
import org.eclipse.jdt.core.dom.StructuralPropertyDescriptor;
import org.eclipse.jdt.core.dom.SuperConstructorInvocation;
import org.eclipse.jdt.core.dom.SuperMethodInvocation;
import org.eclipse.jdt.core.dom.ThrowStatement;
import org.eclipse.jdt.core.dom.TypeLiteral;
import org.eclipse.jdt.core.dom.VariableDeclaration;
import org.eclipse.jdt.core.dom.VariableDeclarationFragment;
import org.eclipse.jdt.core.dom.Assignment.Operator;

import com.googlecode.syper.javasyp.checker.IChecker.Category;

/**
 * @author kevin
 *
 */
public class SymbolicMethodVisitor extends ASTVisitor {

	private IChecker checker;

	/** Points to the top of the scope stack */
	private Scope scopeStack;

	/** <code>null</code> for static methods */
	private ITypeBinding receiver;

	/** Signature of the analyzed method, populated by {@link #visit(MethodDeclaration)} */
	private MethodDeclaration method;

	public SymbolicMethodVisitor() {
		// default scope
		scopeStack = new Scope();
	}

	/**
	 * Override this method to return millis spent in external solvers.
	 * The default implementation always returns 0.
	 * @return millis spent in external solvers, never negative
	 */
	public long getSolverMillis() {
		return 0;
	}

	public void setChecker(IChecker checker) {
		this.checker = checker;
	}

	protected IChecker getChecker() {
		return checker;
	}

	public void setReceiver(ITypeBinding receiver) {
		this.receiver = receiver;
	}

	protected ITypeBinding getReceiver() {
		if (getMethod() == null || isStatic(getMethod().resolveBinding()))
			return null;
		return receiver;
	}

	protected IMethodBinding getSignature() {
		// TODO walk scope stack instead to be resilient against nested methods
		return method.resolveBinding();
	}

	protected MethodDeclaration getMethod() {
		return method;
	}

	protected PermKind getEffectivePerm(Expression e) {
		if (e == null)
			return getCurrentScope().getEffectiveReceiverPerm(receiver);
		return getCurrentScope().getEffectiveType(e).getPerm();
	}

	/**
	 * Returns all locals and receiver fields with their permissions,
	 * which are possibly {@code null} (i.e., {@code null} values will
	 * appear in the map for all variables and fields without permissions.
	 * @return
	 */
	protected Map<IVariableBinding, PermKind> getLocalsAndReceiverFields() {
		if (getCurrentScope() == null)
			return Collections.emptyMap();
		return getCurrentScope().getLocalsAndReceiverFields(true);
	}

	protected final boolean isReceiverProtects() {
		PermKind receiverPerm = getCurrentScope().getExposedReceiverPerm();
		if (receiverPerm == null)
			receiverPerm = getReceiverPerm();
		return receiverPerm != null && receiverPerm.isProtection();
	}

	protected PermKind getReceiverPerm() {
		if (getCurrentScope() == null || receiver == null)
			return null;
		return getCurrentScope().getEffectiveReceiverPerm(receiver);
	}

	@Override
	public boolean visit(MethodDeclaration node) {
		method = node;
		if (Modifier.isStatic(node.getModifiers()))
			receiver = null;
		else
			receiver = node.resolveBinding().getDeclaringClass();
		Scope s = prepareScopeVisit(node);

		if (node.isConstructor()) {
			// inject exclusive receiver permission into constructors
			// constructor works with exposed receiver...
			s.setExposedReceiver(PermKind.EXCL);
			// fill with field permissions, since they're all null to start with
			// TODO field initializers....
			for (IVariableBinding f : receiver.getDeclaredFields()) {
				if (isStatic(f))
					// ignore static fields
					continue;
				RefType info = checker.getVariableType(f);
				if (info == null)
					// no permission declared for field f
					continue;
				s.put(f, info);
			}
			return super.visit(node);
		}

		IMethodBinding binding = node.resolveBinding();
		if (! Modifier.isStatic(node.getModifiers())) {
			// inject declared receiver permission into instance methods
			getCurrentScope().putReceiver(receiver, checker.getReceiverType(binding));
		} else if (checker.getReceiverType(binding) != null) {
			// permission annotation on static method is a syntax error
			checker.reportUserProblem(
					"Receiver annotation invalid on non-instance method",
					node, Category.SYNTAX);
		}
		// arguments will be injected by visit(SingleVariableDeclaration)
		return super.visit(node);
	}

	@Override
	public void endVisit(MethodDeclaration node) {
		endScopeVisit(node, node.isConstructor());
		super.endVisit(node);
		receiver = null;
		method = null;
	}

	@Override
	public void endVisit(ReturnStatement node) {
		// consume return value here
		// parameters are checked in endVisit(MethodDeclaration)
		RefType p = checker.getReturnType(getSignature());
		if (p != null && node.getExpression() != null) {
			try {
				getCurrentScope().consume(node.getExpression(), p, node);
			} catch (PermissionException e) {
				checker.reportUserProblem(e.getLocalizedMessage(), node, Category.POST);
			}
			if (p.isBorrowed())
				getCurrentScope().release(node.getExpression(), p.getPerm(), node);
		}
		super.endVisit(node);
	}

	@Override
	public void endVisit(ThrowStatement node) {
		// TODO Auto-generated method stub
		super.endVisit(node);
	}

	//////////////////////////////////////////////////
	//
	//  Assignments and declarations
	//
	//////////////////////////////////////////////////

	@Override
	public void endVisit(Assignment node) {
		if (Operator.ASSIGN.equals(node.getOperator())) {
			try {
				getCurrentScope().assign(node.getRightHandSide(), node.getLeftHandSide());
			} catch (PermissionException e) {
				checker.reportUserProblem(e.getLocalizedMessage(), node, Category.LOCALS);
			}
		} // else primitive or string ops, which we can ignore :)

		// release left-hand side, which we suppressed in postVisit()
		releaseChildrenIfTemp(node.getLeftHandSide());
		super.endVisit(node);
	}

	@Override
	public void endVisit(SingleVariableDeclaration node) {
		endVisitVarDecl(node);
		super.endVisit(node);
	}

	@Override
	public void endVisit(VariableDeclarationFragment node) {
		endVisitVarDecl(node);
		super.endVisit(node);
	}

	private void endVisitVarDecl(VariableDeclaration node) {
		IVariableBinding binding = node.resolveBinding();
		if (binding == null || binding.isField())
			return;
		RefType p = checker.getLocalType(node);
		try {
			if (p != null && p.isReleased() && ! binding.isParameter())
				checker.reportUserProblem(
						"Cannot use \"released\" on local variables",
						node, Category.SYNTAX);
			getCurrentScope().put(node, p);
		} catch (PermissionException e) {
			checker.reportUserProblem(e.getLocalizedMessage(), node, Category.PRE);
		}
	}

	//////////////////////////////////////////////////
	//
	//  Invocations
	//
	//////////////////////////////////////////////////

	@Override
	@SuppressWarnings("unchecked")
	public void endVisit(ClassInstanceCreation node) {
		handleInvocation(node, node.resolveConstructorBinding(),
				node.getExpression(), // outer object
				node.arguments(),     // arguments
				null);                // TODO implicit outer object
		// inject exclusive permission for new object
		// do this here so we can handle constructor invocations properly
//		getCurrentScope().put(node, PermKind.EXCL);
		super.endVisit(node);
	}

	@Override
	@SuppressWarnings("unchecked")
	public void endVisit(ConstructorInvocation node) {
		IMethodBinding binding = node.resolveConstructorBinding();
		handleInvocation(node, binding,
				null,             // no receiver
				node.arguments(), // arguments
				null);            // TODO implicit outer object
		super.endVisit(node);
	}

	@Override
	@SuppressWarnings("unchecked")
	public void endVisit(MethodInvocation node) {
		IMethodBinding binding = node.resolveMethodBinding();
		handleInvocation(node, binding,
				node.getExpression(), // receiver
				node.arguments(),     // arguments
				node.getExpression() == null ? getImplicitReceiver(binding) : node.getExpression().resolveTypeBinding());
		super.endVisit(node);
	}

	protected final ITypeBinding getImplicitReceiver(IMethodBinding binding) {
		// TODO implement correct receiver resolution for inner classes
		return receiver;
	}

	@Override
	@SuppressWarnings("unchecked")
	public void endVisit(SuperConstructorInvocation node) {
		IMethodBinding binding = node.resolveConstructorBinding();
		handleInvocation(node, binding,
				node.getExpression(), // outer object
				node.arguments(),     // arguments
				null);                // TODO implicit outer object
		super.endVisit(node);
	}

	@Override
	@SuppressWarnings("unchecked")
	public void endVisit(SuperMethodInvocation node) {
		IMethodBinding binding = node.resolveMethodBinding();
		handleInvocation(node, binding,
				null,                         // receiver encoded in invocation target
				node.arguments(),             // arguments
				binding.getDeclaringClass()); // invocation target
		super.endVisit(node);
	}

	private void handleInvocation(ASTNode node, IMethodBinding binding,
			Expression receiver, List<Expression> arguments,
			ITypeBinding receiverType) {
		final Scope s = getCurrentScope();
		boolean capturesFieldsOnly = true;

		// 1. pre-condition checking

		// 1.a receiver / outer object (for constructor)
		if (binding.isConstructor()) {
			// TODO supported outer object
			if (receiver != null) {
				checker.reportUserProblem("Outer objects not currently supported",
						node, Category.UNSUPPORTED);
			}
		} else if (! isStatic(binding)) {
			RefType p = checker.getReceiverType(binding);
			if (p != null) {
				try {
					if (receiver == null) {
						// implicit receiver
						s.consumeReceiver(receiverType, p.getPerm(),
								p.isConsumed() ? null : node);
					} else {
						// explicit receiver expression
						s.consume(receiver, p, node);
						if (p.isReleased() && (!(receiver instanceof SimpleName) || !((IVariableBinding) ((SimpleName) receiver).resolveBinding()).isField()))
							capturesFieldsOnly = false;
					}
				} catch (PermissionException e) {
					checker.reportUserProblem(e.getLocalizedMessage(),
							receiver != null ? receiver : node,
							Category.PRE);
				}
			}
		}
		int i = 0;
		for (Expression arg : arguments) {
			// 1.b Arguments
			RefType p = checker.getParamType(binding, i++);
			if (p == null)
				continue;
			if (p.isReleased())
				capturesFieldsOnly = true;
			try {
				s.consume(arg, p, node);
			} catch (PermissionException e) {
				checker.reportUserProblem(e.getLocalizedMessage(), arg, Category.PRE);
			}
		}

		// 2. Post-condition assumption

		// 2.a inject result permission
		if (node instanceof Expression) {
			// TODO do not *require* capturing expression to be borrowed
			// see SymbolicChecker.getReturnType
			RefType returnType = checker.getReturnType(binding);
			if (returnType != null) {
//				if (returnType.isBorrowed() && capturesFieldsOnly)
//					s.put((Expression) node, ObjectType.getInstance(returnType.getPerm(), false, true, returnType.getElemDims()));
//				else
					s.put((Expression) node, returnType);
			}
		} // else this would be a constructor or super-constructor invocation

		if (! binding.isConstructor() && ! isStatic(binding)) {
			// 2.b receiver
			RefType p = checker.getReceiverType(binding);
			if (p != null) {
				if (receiver == null) {
					// receiver implicit
					if (p.isBorrowed())
						s.releaseReceiver(receiverType, p.getPerm(), node);
					else if (p.isReleased())
						s.disableReceiver(receiverType, node);
				} else {
					if (p.isBorrowed())
						s.release(receiver, p.getPerm(), node);
					else if (p.isReleased())
						s.disable(receiver, node);
				}
			}
		}
		i = 0;
		for (Expression arg : arguments) {
			// 2.c arguments
			RefType p = checker.getParamType(binding, i++);
			if (p == null)
				continue;
			if (p.isBorrowed()) {
				s.release(arg, p.getPerm(), node);
			} else if (p.isReleased()) {
				s.disable(arg, node);
			}
		}
	}

	/**
	 * Returns whether the given binding is declared {@code static}
	 * @param binding never {@code null}
	 * @return {@code true} if the binding is declared {@code static},
	 * {@code false} otherwise
	 * @see Modifier#isStatic(int)
	 */
	protected static boolean isStatic(IBinding binding) {
		return Modifier.isStatic(binding.getModifiers());
	}

	////////////////////////////////////////////////////
	//
	//  Literals
	//
	////////////////////////////////////////////////////

	@Override
	public void endVisit(BooleanLiteral node) {
		// immutable if this thing gets unboxed
		getCurrentScope().put(node, PermKind.IMM);
		super.endVisit(node);
	}

	@Override
	public void endVisit(NullLiteral node) {
		// null can be anything
		getCurrentScope().put(node, PermKind.EXCL);
		super.endVisit(node);
	}

	@Override
	public void endVisit(NumberLiteral node) {
		// immutable if this thing gets unboxed
		getCurrentScope().put(node, PermKind.IMM);
		super.endVisit(node);
	}

	@Override
	public void endVisit(StringLiteral node) {
		getCurrentScope().put(node, PermKind.IMM);
		super.endVisit(node);
	}

	@Override
	public void endVisit(TypeLiteral node) {
		getCurrentScope().put(node, PermKind.IMM);
		super.endVisit(node);
	}

	////////////////////////////////////////////////////
	//
	//  Blocks and block-like (for) loops
	//
	////////////////////////////////////////////////////

	@Override
	public boolean visit(Block node) {
//		if (!(node.getParent() instanceof LabeledStatement) ||
//				PermKind.valueOrNull(((LabeledStatement) node.getParent()).getLabel().getIdentifier().toUpperCase()) == null)
			prepareScopeVisit(node);
		return super.visit(node);
	}

	@Override
	public void endVisit(Block node) {
//		if (!(node.getParent() instanceof LabeledStatement) ||
//				PermKind.valueOrNull(((LabeledStatement) node.getParent()).getLabel().getIdentifier().toUpperCase()) == null)
			endScopeVisit(node);
		super.endVisit(node);
	}

	@Override
	public boolean visit(EnhancedForStatement node) {
		prepareScopeVisit(node);
		return super.visit(node);
	}

	@Override
	public void endVisit(EnhancedForStatement node) {
		endScopeVisit(node);
		super.endVisit(node);
	}

	@Override
	public boolean visit(ForStatement node) {
		prepareScopeVisit(node);
		return super.visit(node);
	}

	@Override
	public void endVisit(ForStatement node) {
		endScopeVisit(node);
		super.endVisit(node);
	}

	protected Scope prepareScopeVisit(ASTNode node) {
		return pushScope(node);
	}

	private void endScopeVisit(ASTNode node) {
		endScopeVisit(node, false);
	}

	private void endScopeVisit(ASTNode node, boolean isConstructor) {
		Scope s = popScope();
		try {
			s.releaseScopeVariables(isConstructor);
		} catch (PermissionException e) {
			checker.reportUserProblem(e.getLocalizedMessage(), node, Category.LOCALS);
		}
	}

	/**
	 * Returns the currently active scope
	 * @return the currently active scope
	 */
	protected Scope getCurrentScope() {
		return scopeStack;
	}

	/**
	 * Use this with care--sets the current scope, which must be for the same
	 * {@link Scope#getBlock() block} as the currently used scope.
	 * @param s
	 * @return previous scope
	 */
	protected Scope setCurrentScope(Scope s) {
		if (s == null) {
			if (scopeStack != null)
				throw new IllegalStateException();
			return null;
		}
		Scope result = scopeStack;
		if (! s.getBlock().equals(result.getBlock()))
			throw new IllegalStateException("Scopes for different nodes: " +
					result.getBlock() + " vs " + s.getBlock());
		scopeStack = s;
		return result;
	}

	/**
	 * Returns the new top of the scope stack
	 * @param block
	 * @return the new top of the scope stack
	 */
	private Scope pushScope(ASTNode block) {
		scopeStack = new Scope(scopeStack, block);
		return scopeStack;
	}

	/**
	 * Returns the popped scope
	 * @return the popped scope
	 */
	protected Scope popScope() {
		Scope result = scopeStack;
		scopeStack = result.getParent();
		return result;
	}

	//////////////////////////////////////////////
	//
	//  Wrapper expressions
	//
	//////////////////////////////////////////////

	@Override
	public void endVisit(CastExpression node) {
		getCurrentScope().capture(node.getExpression(), node);
		super.endVisit(node);
	}

	@Override
	public void endVisit(ParenthesizedExpression node) {
		getCurrentScope().capture(node.getExpression(), node);
		super.endVisit(node);
	}

	@Override
	public void endVisit(ConditionalExpression node) {
		Scope s = getCurrentScope();
		RefType p1 = s.getEffectiveType(node.getThenExpression());
		RefType p2 = s.getEffectiveType(node.getElseExpression());
		if (p1 != null && p2 != null) {
			RefType joined = p1.join(p2);
			try {
				s.consume(node.getThenExpression(), joined, node);
				s.consume(node.getElseExpression(), joined, node);
			} catch (PermissionException e) {
				throw new IllegalStateException("this should never happen", e);
			}
			s.put(node, joined);
			s.disable(node.getThenExpression(), node);
			s.disable(node.getElseExpression(), node);
		}
		super.endVisit(node);
	}

	//////////////////////////////////////////////
	//
	//  Fields...
	//
	//////////////////////////////////////////////

	@Override
	public boolean visit(LabeledStatement node) {
		PermKind p = PermKind.valueOrNull(node.getLabel().getIdentifier().toUpperCase());
		if (p != null) {
			Scope s = pushScope(node);
			s.setExposedReceiver(p);
			try {
				s.consumeReceiver(receiver, p, node);
			} catch (PermissionException e) {
				checker.reportUserProblem(
						"Cannot unpack: " + e.getLocalizedMessage(),
						node, Category.EXPOSURE);
			}
			// put field permissions in no matter what to keep going
			for (IVariableBinding f : receiver.getDeclaredFields()) {
				RefType info = checker.getVariableType(f);
				if (info == null)
					// no permission declared for field f
					continue;
				s.put(f, info.leak(p));
			}
		}
		return super.visit(node);
	}

	@Override
	public void endVisit(LabeledStatement node) {
		PermKind p = PermKind.valueOrNull(node.getLabel().getIdentifier().toUpperCase());
		if (p != null) {
			Scope s = popScope();
			try {
				// will *not* release fields
				// that's crucial since fields are effectively consumed here
				s.releaseScopeVariables();
			} catch (PermissionException e) {
				// this means we can't release the receiver...
				if (! s.isReceiverConsumable(receiver)) {
					// ah this is bad, we're supposed to return the receiver perm
					// produce error here so user has a clue why this happens
					checker.reportUserProblem("Receiver permission consumed: " + e.getLocalizedMessage(),
							node.getLabel(), Category.EXPOSURE);
				}
				return;
			}
			// outside try-catch in case releaseReceiver starts throwing
			s.releaseReceiver(receiver, p, node);
		}
	}

	///////////////////////////////////////////////////////
	//
	// Arrays
	//
	///////////////////////////////////////////////////////

	@Override
	public void endVisit(ArrayAccess node) {
		Scope s = getCurrentScope();
		s.accessArrayElement(node);
	}

	@Override
	public void endVisit(ArrayCreation node) {
		// exclusive permission for newly created array
		if (node.getInitializer() != null) {
			// use permission from initializer...
			getCurrentScope().capture(node.getInitializer(), node);
		} else {
			// excl for all dimensions
			// Java 7 will let us do this better
			int dimCount = node.getType().getDimensions();
			PermKind[] dims = new PermKind[dimCount];
			Arrays.fill(dims, PermKind.EXCL);
			if (node.getType().getElementType().isPrimitiveType())
				// assume immutable permission for primitives
				// TODO immutable perm for Integer etc.
				dims[dimCount - 1] = PermKind.IMM;
			// excl permission for newly constructed array
			getCurrentScope().put(node,
					ObjectType.getInstance(PermKind.EXCL, false, false, dims));
		}
		super.endVisit(node);
	}

	@Override
	@SuppressWarnings("unchecked")
	public void endVisit(ArrayInitializer node) {
		Scope s = getCurrentScope();

		// infer array dimension perms from initializer expressions
		PermKind[] dims = new PermKind[node.resolveTypeBinding().getDimensions()-1];
		Arrays.fill(dims, PermKind.EXCL);
		RefType strongest = ObjectType.getInstance(PermKind.EXCL, false, false, dims);
		for (Expression e : (List<Expression>) node.expressions()) {
			RefType t = s.getEffectiveType(e);
			if (t == null) {
				strongest = null;
				break;
			}
			if (! t.isStrongerThan(strongest))
				strongest = t;
		}
		// if we made it here then all elements have a perm

		PermKind[] newDims;
		if (strongest == null) {
			newDims = new PermKind[0];
		} else {
			PermKind toConsume = strongest.getPerm();
			newDims = new PermKind[dims.length + 1];
			System.arraycopy(strongest.getElemDims(), 0, newDims, 1, dims.length);
			newDims[0] = toConsume;
		}
		s.put(node, ObjectType.getInstance(PermKind.EXCL /* new array */, false, false, newDims));

		if (strongest != null) {
			for (Expression e : (List<Expression>) node.expressions()) {
				try {
					s.consume(e, strongest, node);
				} catch (PermissionException e1) {
					// this shouldn't happen since we used the greatest common
					// denominator
					throw new IllegalStateException("could not consume "
							+ strongest + " from " + e, e1);
				}
				s.disable(e, node);
			}
		}
		super.endVisit(node);
	}

	///////////////////////////////////////////////////////
	//
	// Branches
	//
	///////////////////////////////////////////////////////

	/**
	 * Do not override this method without including this code there.
	 * {@inheritDoc}
	 * @param node {@inheritDoc}
	 */
	@Override
	public boolean visit(IfStatement node) {
		boolean result = super.visit(node);
		if (node.getElseStatement() == null)
			return result;

		node.getExpression().accept(this);
		Scope saveScope = new Scope(getCurrentScope());

		// continue using current scope for then-branch
		prepareScopeVisit(node.getThenStatement());
		node.getThenStatement().accept(this);
		Scope thenScope = popScope();

		// start fresh for else-branch
		scopeStack = saveScope;
		prepareScopeVisit(node.getElseStatement());
		node.getElseStatement().accept(this);
		Scope elseScope = popScope();

		try {
			elseScope.mergeIn(thenScope);
		} catch (PermissionException e) {
			getChecker().reportUserProblem(e.getLocalizedMessage(),
					node, Category.LOCALS);
		}
		return false;
	}

	///////////////////////////////////////////////////////
	//
	// Post-visit
	//   generic release operation after every expression
	///////////////////////////////////////////////////////

	@Override
	public void postVisit(ASTNode node) {
		// restriction to expressions is an optimization
		if (node instanceof Expression || node instanceof ExpressionStatement) {
			// try to release children of this node
			// not useful to release this node since its permission may be
			// needed for parent node
			// TODO check if child properties are of Expression (sub-)type for efficiency

			if (node.getParent() instanceof Assignment && ((Assignment) node.getParent()).getLeftHandSide() == node)
				// in an assignment we need the dereferenced object to stick around, if any
				// (object or array for field or array cell assignment, respectively)
				// otherwise we can't do a[0][0] = 5 (see NestedLocalArrays test)
				// we'll release these children in endVisit(Assignment)
				// this is unnecessary and has no effect if the left-hand side is a local variable
				// or the dereferenced object is a local or field
				return;

			releaseChildrenIfTemp(node);
		}
		super.postVisit(node);
	}

	@SuppressWarnings("unchecked")
	private void releaseChildrenIfTemp(ASTNode node) {
		for (StructuralPropertyDescriptor p :
				(List<StructuralPropertyDescriptor>) node.structuralPropertiesForType()) {
			if (p instanceof ChildPropertyDescriptor) {
				getCurrentScope().releaseIfTemp(
						(ASTNode) node.getStructuralProperty(p));
			} else if (p instanceof ChildListPropertyDescriptor) {
				for (ASTNode child :
						(List<ASTNode>) node.getStructuralProperty(p))
					getCurrentScope().releaseIfTemp(child);
			}
		}
	}
}
